Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    minus(x,0)  → x
2:    minus(s(x),s(y))  → minus(x,y)
3:    quot(0,s(y))  → 0
4:    quot(s(x),s(y))  → s(quot(minus(x,y),s(y)))
5:    plus(0,y)  → y
6:    plus(s(x),y)  → s(plus(x,y))
7:    plus(minus(x,s(0)),minus(y,s(s(z))))  → plus(minus(y,s(s(z))),minus(x,s(0)))
There are 5 dependency pairs:
8:    MINUS(s(x),s(y))  → MINUS(x,y)
9:    QUOT(s(x),s(y))  → QUOT(minus(x,y),s(y))
10:    QUOT(s(x),s(y))  → MINUS(x,y)
11:    PLUS(s(x),y)  → PLUS(x,y)
12:    PLUS(minus(x,s(0)),minus(y,s(s(z))))  → PLUS(minus(y,s(s(z))),minus(x,s(0)))
The approximated dependency graph contains 3 SCCs: {8}, {11,12} and {9}.
Tyrolean Termination Tool  (0.04 seconds)   ---  May 4, 2006